ds:x:Id fp Type, a, b:kz:KndId fp Top.
update-spec-decl(a;ds)  update-spec-decl(b;ds)  update-spec-decl(a  b;ds) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, x:AB(x), Top, x.A(x), x:AB(x), type List, update-spec-vars(upd), IdDeq, x  dom(f), b, Prop, (x  l), P  Q, a  b, update-spec-decl(upd;ds), left+right, P  Q, P & Q, P  Q, KindDeq, product-deq(A;B;a;b), f  g, fpf-domain(f), 2of(t), map(f;as)
Lemmas	map wf, pi2 wf, fpf-domain wf, fpf-join wf, product-deq wf, Kind-deq wf, update-spec-join-vars, l member wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, top wf, Knd wf, fpf wf, Id wf